Nuprl Lemma : double_sum_wf
4,23
postcript
pdf
n
,
m
:
,
f
:(
n
m
). sum(
f
(
x
,
y
) |
x
<
n
;
y
<
m
)
latex
Definitions
sum(
f
(
x
;
y
) |
x
<
n
;
y
<
m
)
,
sum(
f
(
x
) |
x
<
k
)
,
x
.
t
(
x
)
,
x
(
s1
,
s2
)
,
{
i
..
j
}
,
x
:
A
.
B
(
x
)
,
t
T
,
Lemmas
nat
wf
,
int
seg
wf
,
sum
wf
origin
n, m:
, f:(n
m
). sum(f(x,y) | x < n; y < m) 
n, m:, f:(nm). sum(f(x,y) | x < n; y < m) 
x. t(x)
}x:A. B(x) T